Repository navigation
Fix treap map/list bugs, tighten Treapability rule, expand tests - #29
Merged
Merged
Conversation
The existing suite left merge, update, parallel bulk ops, set algebra, list builders, and much of the treapability rule unexercised. These tests raise JaCoCo line coverage of com.certora.collect from 60.5% to 91.2%. Product bugs are pinned with ignored tests so the suite stays green. Copy-constructor and negative-query tests were comparing the wrong collections. Proved with the Gradle test tasks and a JaCoCo run. HashTreapMap mutation testing killed all 80 covered mutants. Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
Raise test coverage and record known collection bugs
getShallowMerger treated a null value as a missing key, so a key present with a null value was merged twice and could be stored twice in the bucket. Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
Fix union merge of hash-treap null values
The null-key, hash-key, copy-constructor, and iterator-removal cases were the same assertions with different arguments. Each scenario still runs, through one helper instead of a copied method. Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: ericeil <7407587+ericeil@users.noreply.github.com>
The size was copied once in the constructor, so add and clear left it stale while isEmpty read the updated list. Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
A hashCode body that returns a property directly was skipped because the reference has no parent call. Object diagnostics also named a utils.treapHashObject helper that does not exist. Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
set replaced the element in the builder but left the iterator on the previous treap, so previous still returned the old value. Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
fallbackUnion and fallbackIntersect forced the stored value with !!, so a null value threw NullPointerException before the merger ran. Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
parallelMerge, parallelUnion, and parallelIntersect subtracted one before the size check, so a threshold of 0 asked for a negative log and threw. Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
* Seed TreapList priorities so test coverage is reproducible Node priorities came from Random.Default, so each JVM run built a different tree and JaCoCo instruction coverage for getNodeAt and computeHashCode moved between runs. Tests now install a seeded generator, with one fixed tree for the branches a single random shape can miss. Production still uses Random.Default when the override is null. Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com> * Keep TreapList priority seeds on the test thread The shared Random required tests in one JVM not to overlap, and ProductBugTest still built lists from Random.Default. Each test method that builds a TreapList now gets its own seeded generator on the thread that runs it. Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com> --------- Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
…layout (#10) * Reset TreapListBuilder iterator state after add and remove. The builder's list iterator kept lastReturnedIndex after add() and remove(), so a following set() or remove() acted on whichever element had shifted into that index instead of throwing IllegalStateException as the ListIterator contract requires. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * Exempt explicit and parenthesized TreapableHashCode.plus arguments. The Treapability hashCode check exempted a property only when its direct parent resolved to TreapableHashCode.plus. That covered `it + e` but not `it.plus(e)` (the parent is a value argument) or `it + (e)` (the parent is a parenthesized expression), so both were reported. Look through parentheses and from a value argument to its call before resolving. Also fix a stale 'utils.HashCode.plus' reference in the rule's comment. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * Describe the code, not the change, in recent comments. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * Move ProductBugTest cases next to the behavior they cover. The map cases now live in TreapMapTest, so they run against both the hashed and sorted implementations (the null-value collision case stays in HashTreapMapTest). The parallel zero-threshold case uses the same larger maps as the existing parallel test. The list builder cases move to TreapListTest. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fixes several bugs found while expanding test coverage, tightens the Treapability detekt rule, and makes the TreapList tests reproducible.
PR numbers in the commit titles (e.g. "(#3)") are pull requests on the fork
ericeil/certora-collections, not on this repo.Bug fixes
null.HashTreapMap's shallow merger calledshallowGetValueto decide whether a key was missing from the left side. That function returnsnullboth for a missing key and for a storednull, so a key stored with anullvalue was merged twice. It now checksshallowContainsKey.union/intersectwith a plainMapthrewNullPointerException(this[k]!!) when a key that both maps share had anullvalue on the treap side.parallelThresholdLog2 = 0threwIllegalArgumentException, because the threshold minus one was passed as a negative log. A threshold of 0 is now accepted.TreapListBuilder.sizewas captured when the builder was created and never updated.TreapListBuilderlist iterator:set()replaced the builder's list but kept iterating the old one, so the iterator didn't see its own write.add()andremove()didn't clear the last-returned position, so a followingset()orremove()changed the wrong element instead of throwingIllegalStateException.Treapability detekt rule
hashCode()body that uses a property outside of any call (e.g.hashCode(): Int = b) or passes it to another function (e.g.Objects.hash(e)) is now checked. Before, it was skipped.TreapableHashCode.plusis exempt whether writtenit + e,it.plus(e), orit + (e).treapHashObjectinstead of the oldutils.treapHashObject.Tests
TreapableHashCodeoperations, with shared helpers for map and set tests that were repeated.TreapListNode.setTreapListPriorityRandom). A JUnit rule,TreapListPriorityRule, seeds it for each test, so TreapList shapes and coverage are the same on every run. Production code still usesRandom.Default.Testing
./gradlew testpasses.🤖 Generated with Claude Code